Section: New Results

Static Analysis of Bit-Level Machine Integer and Floating-Point Operations

Participant : Antoine Miné.

Abstract interpretation, Embedded software, Numerical abstract domains, Run-time errors, Static analysis.

We present in [22] a few lightweight numeric abstract domains to analyze C programs that exploit the binary representation of numbers in computers, for instance to perform "compute-through-overflow" on machine integers, or to directly manipulate the exponent and mantissa of floating-point numbers. On integers, we propose an extension of intervals with a modular component, as well as a bitfield domain. On floating-point numbers, we propose a predicate domain to match, infer, and propagate selected expression patterns. These domains are simple, efficient, and extensible. We have included them into the Astrée ( 5.2 ) and AstréeA ( 5.3 ) static analyzers to supplement existing domains. Experimental results show that they can improve the analysis precision at a reasonable cost.